COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		The idea of regarding program variables as explicit functions
C00004 00003	Notes on conversation with Tang
C00005 00004	axiom stepdef:	∀j.(phi1(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m*(n - i(t))
C00006 ENDMK
C⊗;
	The idea of regarding program variables as explicit functions
of time and regarding the program counter as just another variable
has cropped up in a number of recent papers.  However, so far as I know,
it has always been discussed as a means of proving facts about
programs rather than as the primary representation of the program
itself.  Uniformly, explicit mention of time and the program
counter has been deplored.  Francez (1978) calls it "nasty" and
had difficulty getting his paper using the technique to prove
correctness of the Dijkstra garbage collector published.  Ashcroft
(1979) refers to it negatively.

	Having implicitly rejected the approach several times myself,

	I always implicitly rejected the approach myself and only
"backed into it" through wanting to allow programs that refer to the
past.  However, I now think that always
avoiding explicit mention of time and the program counter
constitutes a commitment
to proving programs with one hand tied behind one's back.
Notes on conversation with Tang

1. Elephant can be used for giving the operational semantics
of other languages.

2. reduced Elephant like language ?

3. Ma compiled to E ?

4. Tang correspondence between control and data structures ?
axiom stepdef:	∀j.(phi1(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m*(n - i(t))
	∧ i(t) = j)
		⊃ ∃t.(pc(t) = done ∧ p(t) = m*n));;

∧i stepdef[phi←λj.phi1(j)];